YES 0.675 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/FiniteMap.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



↳ HASKELL
  ↳ LR

mainModule FiniteMap
  ((addToFM :: FiniteMap () a  ->  ()  ->  a  ->  FiniteMap () a) :: FiniteMap () a  ->  ()  ->  a  ->  FiniteMap () a)

module FiniteMap where
  import qualified Maybe
import qualified Prelude
  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a) 
  instance (Eq a, Eq b) => Eq (FiniteMap b a) where 
  addToFM :: Ord b => FiniteMap b a  ->  b  ->  a  ->  FiniteMap b a
addToFM fm key elt = addToFM_C (\old new ->new) fm key elt

  addToFM_C :: Ord a => (b  ->  b  ->  b)  ->  FiniteMap a b  ->  a  ->  b  ->  FiniteMap a b
addToFM_C combiner EmptyFM key elt = unitFM key elt
addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt 
 | new_key < key = 
mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r
 | new_key > key = 
mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)
 | otherwise = 
Branch new_key (combiner elt new_elt) size fm_l fm_r

  emptyFM :: FiniteMap a b
emptyFM = EmptyFM

  findMax :: FiniteMap a b  ->  (a,b)
findMax (Branch key elt _ _ EmptyFM) = (key,elt)
findMax (Branch key elt _ _ fm_r) = findMax fm_r

  findMin :: FiniteMap a b  ->  (a,b)
findMin (Branch key elt _ EmptyFM _) = (key,elt)
findMin (Branch key elt _ fm_l _) = findMin fm_l

  mkBalBranch :: Ord b => b  ->  a  ->  FiniteMap b a  ->  FiniteMap b a  ->  FiniteMap b a
mkBalBranch key elt fm_L fm_R 
 | size_l + size_r < 2 = 
mkBranch 1 key elt fm_L fm_R
 | size_r > sIZE_RATIO * size_l = 
case fm_R of
  Branch _ _ _ fm_rl fm_rr
 | sizeFM fm_rl < 2 * sizeFM fm_rr -> 
single_L fm_L fm_R
 | otherwise -> 
double_L fm_L fm_R
 | size_l > sIZE_RATIO * size_r = 
case fm_L of
  Branch _ _ _ fm_ll fm_lr
 | sizeFM fm_lr < 2 * sizeFM fm_ll -> 
single_R fm_L fm_R
 | otherwise -> 
double_R fm_L fm_R
 | otherwise = 
mkBranch 2 key elt fm_L fm_R where 
double_L fm_l (Branch key_r elt_r _ (Branch key_rl elt_rl _ fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l _ fm_ll (Branch key_lr elt_lr _ fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
single_L fm_l (Branch key_r elt_r _ fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l _ fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l = sizeFM fm_L
size_r = sizeFM fm_R

  mkBranch :: Ord b => Int  ->  b  ->  a  ->  FiniteMap b a  ->  FiniteMap b a  ->  FiniteMap b a
mkBranch which key elt fm_l fm_r = 
let 
result = Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r
in result
 where 
balance_ok = True
left_ok = 
case fm_l of
  EmptyFM-> True
  Branch left_key _ _ _ _-> 
let 
biggest_left_key = fst (findMax fm_l)
in biggest_left_key < key
left_size = sizeFM fm_l
right_ok = 
case fm_r of
  EmptyFM-> True
  Branch right_key _ _ _ _-> 
let 
smallest_right_key = fst (findMin fm_r)
in key < smallest_right_key
right_size = sizeFM fm_r
unbox :: Int  ->  Int
unbox x = x

  sIZE_RATIO :: Int
sIZE_RATIO = 5

  sizeFM :: FiniteMap a b  ->  Int
sizeFM EmptyFM = 0
sizeFM (Branch _ _ size _ _) = size

  unitFM :: a  ->  b  ->  FiniteMap a b
unitFM key elt = Branch key elt 1 emptyFM emptyFM


module Maybe where
  import qualified FiniteMap
import qualified Prelude


Lambda Reductions:
The following Lambda expression
\oldnew→new

is transformed to
addToFM0 old new = new



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR

mainModule FiniteMap
  ((addToFM :: FiniteMap () a  ->  ()  ->  a  ->  FiniteMap () a) :: FiniteMap () a  ->  ()  ->  a  ->  FiniteMap () a)

module FiniteMap where
  import qualified Maybe
import qualified Prelude
  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a) 
  instance (Eq a, Eq b) => Eq (FiniteMap b a) where 
  addToFM :: Ord a => FiniteMap a b  ->  a  ->  b  ->  FiniteMap a b
addToFM fm key elt = addToFM_C addToFM0 fm key elt

  
addToFM0 old new = new

  addToFM_C :: Ord b => (a  ->  a  ->  a)  ->  FiniteMap b a  ->  b  ->  a  ->  FiniteMap b a
addToFM_C combiner EmptyFM key elt = unitFM key elt
addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt 
 | new_key < key = 
mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r
 | new_key > key = 
mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)
 | otherwise = 
Branch new_key (combiner elt new_elt) size fm_l fm_r

  emptyFM :: FiniteMap b a
emptyFM = EmptyFM

  findMax :: FiniteMap a b  ->  (a,b)
findMax (Branch key elt _ _ EmptyFM) = (key,elt)
findMax (Branch key elt _ _ fm_r) = findMax fm_r

  findMin :: FiniteMap b a  ->  (b,a)
findMin (Branch key elt _ EmptyFM _) = (key,elt)
findMin (Branch key elt _ fm_l _) = findMin fm_l

  mkBalBranch :: Ord b => b  ->  a  ->  FiniteMap b a  ->  FiniteMap b a  ->  FiniteMap b a
mkBalBranch key elt fm_L fm_R 
 | size_l + size_r < 2 = 
mkBranch 1 key elt fm_L fm_R
 | size_r > sIZE_RATIO * size_l = 
case fm_R of
  Branch _ _ _ fm_rl fm_rr
 | sizeFM fm_rl < 2 * sizeFM fm_rr -> 
single_L fm_L fm_R
 | otherwise -> 
double_L fm_L fm_R
 | size_l > sIZE_RATIO * size_r = 
case fm_L of
  Branch _ _ _ fm_ll fm_lr
 | sizeFM fm_lr < 2 * sizeFM fm_ll -> 
single_R fm_L fm_R
 | otherwise -> 
double_R fm_L fm_R
 | otherwise = 
mkBranch 2 key elt fm_L fm_R where 
double_L fm_l (Branch key_r elt_r _ (Branch key_rl elt_rl _ fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l _ fm_ll (Branch key_lr elt_lr _ fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
single_L fm_l (Branch key_r elt_r _ fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l _ fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l = sizeFM fm_L
size_r = sizeFM fm_R

  mkBranch :: Ord b => Int  ->  b  ->  a  ->  FiniteMap b a  ->  FiniteMap b a  ->  FiniteMap b a
mkBranch which key elt fm_l fm_r = 
let 
result = Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r
in result
 where 
balance_ok = True
left_ok = 
case fm_l of
  EmptyFM-> True
  Branch left_key _ _ _ _-> 
let 
biggest_left_key = fst (findMax fm_l)
in biggest_left_key < key
left_size = sizeFM fm_l
right_ok = 
case fm_r of
  EmptyFM-> True
  Branch right_key _ _ _ _-> 
let 
smallest_right_key = fst (findMin fm_r)
in key < smallest_right_key
right_size = sizeFM fm_r
unbox :: Int  ->  Int
unbox x = x

  sIZE_RATIO :: Int
sIZE_RATIO = 5

  sizeFM :: FiniteMap a b  ->  Int
sizeFM EmptyFM = 0
sizeFM (Branch _ _ size _ _) = size

  unitFM :: a  ->  b  ->  FiniteMap a b
unitFM key elt = Branch key elt 1 emptyFM emptyFM


module Maybe where
  import qualified FiniteMap
import qualified Prelude


Case Reductions:
The following Case expression
case fm_l of
 EmptyFM → True
 Branch left_key _ _ _ _ → 
let 
biggest_left_key  = fst (findMax fm_l)
in biggest_left_key < key

is transformed to
left_ok0 fm_l key EmptyFM = True
left_ok0 fm_l key (Branch left_key _ _ _ _) = 
let 
biggest_left_key  = fst (findMax fm_l)
in biggest_left_key < key

The following Case expression
case fm_r of
 EmptyFM → True
 Branch right_key _ _ _ _ → 
let 
smallest_right_key  = fst (findMin fm_r)
in key < smallest_right_key

is transformed to
right_ok0 fm_r key EmptyFM = True
right_ok0 fm_r key (Branch right_key _ _ _ _) = 
let 
smallest_right_key  = fst (findMin fm_r)
in key < smallest_right_key

The following Case expression
case fm_R of
 Branch _ _ _ fm_rl fm_rr
 | sizeFM fm_rl < 2 * sizeFM fm_rr
 → single_L fm_L fm_R
 | otherwise
 → double_L fm_L fm_R

is transformed to
mkBalBranch0 fm_L fm_R (Branch _ _ _ fm_rl fm_rr)
 | sizeFM fm_rl < 2 * sizeFM fm_rr
 = single_L fm_L fm_R
 | otherwise
 = double_L fm_L fm_R

The following Case expression
case fm_L of
 Branch _ _ _ fm_ll fm_lr
 | sizeFM fm_lr < 2 * sizeFM fm_ll
 → single_R fm_L fm_R
 | otherwise
 → double_R fm_L fm_R

is transformed to
mkBalBranch1 fm_L fm_R (Branch _ _ _ fm_ll fm_lr)
 | sizeFM fm_lr < 2 * sizeFM fm_ll
 = single_R fm_L fm_R
 | otherwise
 = double_R fm_L fm_R



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR

mainModule FiniteMap
  ((addToFM :: FiniteMap () a  ->  ()  ->  a  ->  FiniteMap () a) :: FiniteMap () a  ->  ()  ->  a  ->  FiniteMap () a)

module FiniteMap where
  import qualified Maybe
import qualified Prelude
  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a) 
  instance (Eq a, Eq b) => Eq (FiniteMap b a) where 
  addToFM :: Ord b => FiniteMap b a  ->  b  ->  a  ->  FiniteMap b a
addToFM fm key elt = addToFM_C addToFM0 fm key elt

  
addToFM0 old new = new

  addToFM_C :: Ord b => (a  ->  a  ->  a)  ->  FiniteMap b a  ->  b  ->  a  ->  FiniteMap b a
addToFM_C combiner EmptyFM key elt = unitFM key elt
addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt 
 | new_key < key = 
mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r
 | new_key > key = 
mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)
 | otherwise = 
Branch new_key (combiner elt new_elt) size fm_l fm_r

  emptyFM :: FiniteMap a b
emptyFM = EmptyFM

  findMax :: FiniteMap b a  ->  (b,a)
findMax (Branch key elt _ _ EmptyFM) = (key,elt)
findMax (Branch key elt _ _ fm_r) = findMax fm_r

  findMin :: FiniteMap b a  ->  (b,a)
findMin (Branch key elt _ EmptyFM _) = (key,elt)
findMin (Branch key elt _ fm_l _) = findMin fm_l

  mkBalBranch :: Ord b => b  ->  a  ->  FiniteMap b a  ->  FiniteMap b a  ->  FiniteMap b a
mkBalBranch key elt fm_L fm_R 
 | size_l + size_r < 2 = 
mkBranch 1 key elt fm_L fm_R
 | size_r > sIZE_RATIO * size_l = 
mkBalBranch0 fm_L fm_R fm_R
 | size_l > sIZE_RATIO * size_r = 
mkBalBranch1 fm_L fm_R fm_L
 | otherwise = 
mkBranch 2 key elt fm_L fm_R where 
double_L fm_l (Branch key_r elt_r _ (Branch key_rl elt_rl _ fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l _ fm_ll (Branch key_lr elt_lr _ fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
mkBalBranch0 fm_L fm_R (Branch _ _ _ fm_rl fm_rr) 
 | sizeFM fm_rl < 2 * sizeFM fm_rr = 
single_L fm_L fm_R
 | otherwise = 
double_L fm_L fm_R
mkBalBranch1 fm_L fm_R (Branch _ _ _ fm_ll fm_lr) 
 | sizeFM fm_lr < 2 * sizeFM fm_ll = 
single_R fm_L fm_R
 | otherwise = 
double_R fm_L fm_R
single_L fm_l (Branch key_r elt_r _ fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l _ fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l = sizeFM fm_L
size_r = sizeFM fm_R

  mkBranch :: Ord b => Int  ->  b  ->  a  ->  FiniteMap b a  ->  FiniteMap b a  ->  FiniteMap b a
mkBranch which key elt fm_l fm_r = 
let 
result = Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r
in result
 where 
balance_ok = True
left_ok = left_ok0 fm_l key fm_l
left_ok0 fm_l key EmptyFM = True
left_ok0 fm_l key (Branch left_key _ _ _ _) = 
let 
biggest_left_key = fst (findMax fm_l)
in biggest_left_key < key
left_size = sizeFM fm_l
right_ok = right_ok0 fm_r key fm_r
right_ok0 fm_r key EmptyFM = True
right_ok0 fm_r key (Branch right_key _ _ _ _) = 
let 
smallest_right_key = fst (findMin fm_r)
in key < smallest_right_key
right_size = sizeFM fm_r
unbox :: Int  ->  Int
unbox x = x

  sIZE_RATIO :: Int
sIZE_RATIO = 5

  sizeFM :: FiniteMap a b  ->  Int
sizeFM EmptyFM = 0
sizeFM (Branch _ _ size _ _) = size

  unitFM :: b  ->  a  ->  FiniteMap b a
unitFM key elt = Branch key elt 1 emptyFM emptyFM


module Maybe where
  import qualified FiniteMap
import qualified Prelude


Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR

mainModule FiniteMap
  ((addToFM :: FiniteMap () a  ->  ()  ->  a  ->  FiniteMap () a) :: FiniteMap () a  ->  ()  ->  a  ->  FiniteMap () a)

module FiniteMap where
  import qualified Maybe
import qualified Prelude
  data FiniteMap a b = EmptyFM  | Branch a b Int (FiniteMap a b) (FiniteMap a b) 
  instance (Eq a, Eq b) => Eq (FiniteMap a b) where 
  addToFM :: Ord b => FiniteMap b a  ->  b  ->  a  ->  FiniteMap b a
addToFM fm key elt = addToFM_C addToFM0 fm key elt

  
addToFM0 old new = new

  addToFM_C :: Ord b => (a  ->  a  ->  a)  ->  FiniteMap b a  ->  b  ->  a  ->  FiniteMap b a
addToFM_C combiner EmptyFM key elt = unitFM key elt
addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt 
 | new_key < key = 
mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r
 | new_key > key = 
mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)
 | otherwise = 
Branch new_key (combiner elt new_elt) size fm_l fm_r

  emptyFM :: FiniteMap b a
emptyFM = EmptyFM

  findMax :: FiniteMap b a  ->  (b,a)
findMax (Branch key elt xw xx EmptyFM) = (key,elt)
findMax (Branch key elt xy xz fm_r) = findMax fm_r

  findMin :: FiniteMap a b  ->  (a,b)
findMin (Branch key elt wy EmptyFM wz) = (key,elt)
findMin (Branch key elt xu fm_l xv) = findMin fm_l

  mkBalBranch :: Ord a => a  ->  b  ->  FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
mkBalBranch key elt fm_L fm_R 
 | size_l + size_r < 2 = 
mkBranch 1 key elt fm_L fm_R
 | size_r > sIZE_RATIO * size_l = 
mkBalBranch0 fm_L fm_R fm_R
 | size_l > sIZE_RATIO * size_r = 
mkBalBranch1 fm_L fm_R fm_L
 | otherwise = 
mkBranch 2 key elt fm_L fm_R where 
double_L fm_l (Branch key_r elt_r zy (Branch key_rl elt_rl zz fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l zw fm_ll (Branch key_lr elt_lr zx fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
mkBalBranch0 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr) 
 | sizeFM fm_rl < 2 * sizeFM fm_rr = 
single_L fm_L fm_R
 | otherwise = 
double_L fm_L fm_R
mkBalBranch1 fm_L fm_R (Branch yz zu zv fm_ll fm_lr) 
 | sizeFM fm_lr < 2 * sizeFM fm_ll = 
single_R fm_L fm_R
 | otherwise = 
double_R fm_L fm_R
single_L fm_l (Branch key_r elt_r vux fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l yy fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l = sizeFM fm_L
size_r = sizeFM fm_R

  mkBranch :: Ord b => Int  ->  b  ->  a  ->  FiniteMap b a  ->  FiniteMap b a  ->  FiniteMap b a
mkBranch which key elt fm_l fm_r = 
let 
result = Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r
in result
 where 
balance_ok = True
left_ok = left_ok0 fm_l key fm_l
left_ok0 fm_l key EmptyFM = True
left_ok0 fm_l key (Branch left_key wu wv ww wx) = 
let 
biggest_left_key = fst (findMax fm_l)
in biggest_left_key < key
left_size = sizeFM fm_l
right_ok = right_ok0 fm_r key fm_r
right_ok0 fm_r key EmptyFM = True
right_ok0 fm_r key (Branch right_key vw vx vy vz) = 
let 
smallest_right_key = fst (findMin fm_r)
in key < smallest_right_key
right_size = sizeFM fm_r
unbox :: Int  ->  Int
unbox x = x

  sIZE_RATIO :: Int
sIZE_RATIO = 5

  sizeFM :: FiniteMap b a  ->  Int
sizeFM EmptyFM = 0
sizeFM (Branch yu yv size yw yx) = size

  unitFM :: a  ->  b  ->  FiniteMap a b
unitFM key elt = Branch key elt 1 emptyFM emptyFM


module Maybe where
  import qualified FiniteMap
import qualified Prelude


Cond Reductions:
The following Function with conditions
addToFM_C combiner EmptyFM key elt = unitFM key elt
addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt
 | new_key < key
 = mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r
 | new_key > key
 = mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)
 | otherwise
 = Branch new_key (combiner elt new_elt) size fm_l fm_r

is transformed to
addToFM_C combiner EmptyFM key elt = addToFM_C4 combiner EmptyFM key elt
addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt

addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r
addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt (new_key > key)

addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)
addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt otherwise

addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt True = Branch new_key (combiner elt new_elt) size fm_l fm_r

addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt (new_key < key)

addToFM_C4 combiner EmptyFM key elt = unitFM key elt
addToFM_C4 vvx vvy vvz vwu = addToFM_C3 vvx vvy vvz vwu

The following Function with conditions
mkBalBranch1 fm_L fm_R (Branch yz zu zv fm_ll fm_lr)
 | sizeFM fm_lr < 2 * sizeFM fm_ll
 = single_R fm_L fm_R
 | otherwise
 = double_R fm_L fm_R

is transformed to
mkBalBranch1 fm_L fm_R (Branch yz zu zv fm_ll fm_lr) = mkBalBranch12 fm_L fm_R (Branch yz zu zv fm_ll fm_lr)

mkBalBranch10 fm_L fm_R yz zu zv fm_ll fm_lr True = double_R fm_L fm_R

mkBalBranch11 fm_L fm_R yz zu zv fm_ll fm_lr True = single_R fm_L fm_R
mkBalBranch11 fm_L fm_R yz zu zv fm_ll fm_lr False = mkBalBranch10 fm_L fm_R yz zu zv fm_ll fm_lr otherwise

mkBalBranch12 fm_L fm_R (Branch yz zu zv fm_ll fm_lr) = mkBalBranch11 fm_L fm_R yz zu zv fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)

The following Function with conditions
mkBalBranch0 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)
 | sizeFM fm_rl < 2 * sizeFM fm_rr
 = single_L fm_L fm_R
 | otherwise
 = double_L fm_L fm_R

is transformed to
mkBalBranch0 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr) = mkBalBranch02 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)

mkBalBranch01 fm_L fm_R vuu vuv vuw fm_rl fm_rr True = single_L fm_L fm_R
mkBalBranch01 fm_L fm_R vuu vuv vuw fm_rl fm_rr False = mkBalBranch00 fm_L fm_R vuu vuv vuw fm_rl fm_rr otherwise

mkBalBranch00 fm_L fm_R vuu vuv vuw fm_rl fm_rr True = double_L fm_L fm_R

mkBalBranch02 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr) = mkBalBranch01 fm_L fm_R vuu vuv vuw fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)

The following Function with conditions
mkBalBranch key elt fm_L fm_R
 | size_l + size_r < 2
 = mkBranch 1 key elt fm_L fm_R
 | size_r > sIZE_RATIO * size_l
 = mkBalBranch0 fm_L fm_R fm_R
 | size_l > sIZE_RATIO * size_r
 = mkBalBranch1 fm_L fm_R fm_L
 | otherwise
 = mkBranch 2 key elt fm_L fm_R
where 
double_L fm_l (Branch key_r elt_r zy (Branch key_rl elt_rl zz fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l zw fm_ll (Branch key_lr elt_lr zx fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
mkBalBranch0 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)
 | sizeFM fm_rl < 2 * sizeFM fm_rr
 = single_L fm_L fm_R
 | otherwise
 = double_L fm_L fm_R
mkBalBranch1 fm_L fm_R (Branch yz zu zv fm_ll fm_lr)
 | sizeFM fm_lr < 2 * sizeFM fm_ll
 = single_R fm_L fm_R
 | otherwise
 = double_R fm_L fm_R
single_L fm_l (Branch key_r elt_r vux fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l yy fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l  = sizeFM fm_L
size_r  = sizeFM fm_R

is transformed to
mkBalBranch key elt fm_L fm_R = mkBalBranch6 key elt fm_L fm_R

mkBalBranch6 key elt fm_L fm_R = 
mkBalBranch5 key elt fm_L fm_R (size_l + size_r < 2)
where 
double_L fm_l (Branch key_r elt_r zy (Branch key_rl elt_rl zz fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l zw fm_ll (Branch key_lr elt_lr zx fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
mkBalBranch0 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr) = mkBalBranch02 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)
mkBalBranch00 fm_L fm_R vuu vuv vuw fm_rl fm_rr True = double_L fm_L fm_R
mkBalBranch01 fm_L fm_R vuu vuv vuw fm_rl fm_rr True = single_L fm_L fm_R
mkBalBranch01 fm_L fm_R vuu vuv vuw fm_rl fm_rr False = mkBalBranch00 fm_L fm_R vuu vuv vuw fm_rl fm_rr otherwise
mkBalBranch02 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr) = mkBalBranch01 fm_L fm_R vuu vuv vuw fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)
mkBalBranch1 fm_L fm_R (Branch yz zu zv fm_ll fm_lr) = mkBalBranch12 fm_L fm_R (Branch yz zu zv fm_ll fm_lr)
mkBalBranch10 fm_L fm_R yz zu zv fm_ll fm_lr True = double_R fm_L fm_R
mkBalBranch11 fm_L fm_R yz zu zv fm_ll fm_lr True = single_R fm_L fm_R
mkBalBranch11 fm_L fm_R yz zu zv fm_ll fm_lr False = mkBalBranch10 fm_L fm_R yz zu zv fm_ll fm_lr otherwise
mkBalBranch12 fm_L fm_R (Branch yz zu zv fm_ll fm_lr) = mkBalBranch11 fm_L fm_R yz zu zv fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)
mkBalBranch2 key elt fm_L fm_R True = mkBranch 2 key elt fm_L fm_R
mkBalBranch3 key elt fm_L fm_R True = mkBalBranch1 fm_L fm_R fm_L
mkBalBranch3 key elt fm_L fm_R False = mkBalBranch2 key elt fm_L fm_R otherwise
mkBalBranch4 key elt fm_L fm_R True = mkBalBranch0 fm_L fm_R fm_R
mkBalBranch4 key elt fm_L fm_R False = mkBalBranch3 key elt fm_L fm_R (size_l > sIZE_RATIO * size_r)
mkBalBranch5 key elt fm_L fm_R True = mkBranch 1 key elt fm_L fm_R
mkBalBranch5 key elt fm_L fm_R False = mkBalBranch4 key elt fm_L fm_R (size_r > sIZE_RATIO * size_l)
single_L fm_l (Branch key_r elt_r vux fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l yy fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l  = sizeFM fm_L
size_r  = sizeFM fm_R

The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed

mainModule FiniteMap
  ((addToFM :: FiniteMap () a  ->  ()  ->  a  ->  FiniteMap () a) :: FiniteMap () a  ->  ()  ->  a  ->  FiniteMap () a)

module FiniteMap where
  import qualified Maybe
import qualified Prelude
  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a) 
  instance (Eq a, Eq b) => Eq (FiniteMap a b) where 
  addToFM :: Ord b => FiniteMap b a  ->  b  ->  a  ->  FiniteMap b a
addToFM fm key elt = addToFM_C addToFM0 fm key elt

  
addToFM0 old new = new

  addToFM_C :: Ord b => (a  ->  a  ->  a)  ->  FiniteMap b a  ->  b  ->  a  ->  FiniteMap b a
addToFM_C combiner EmptyFM key elt = addToFM_C4 combiner EmptyFM key elt
addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt

  
addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt True = Branch new_key (combiner elt new_elt) size fm_l fm_r

  
addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)
addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt otherwise

  
addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r
addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt (new_key > key)

  
addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt (new_key < key)

  
addToFM_C4 combiner EmptyFM key elt = unitFM key elt
addToFM_C4 vvx vvy vvz vwu = addToFM_C3 vvx vvy vvz vwu

  emptyFM :: FiniteMap a b
emptyFM = EmptyFM

  findMax :: FiniteMap b a  ->  (b,a)
findMax (Branch key elt xw xx EmptyFM) = (key,elt)
findMax (Branch key elt xy xz fm_r) = findMax fm_r

  findMin :: FiniteMap b a  ->  (b,a)
findMin (Branch key elt wy EmptyFM wz) = (key,elt)
findMin (Branch key elt xu fm_l xv) = findMin fm_l

  mkBalBranch :: Ord a => a  ->  b  ->  FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
mkBalBranch key elt fm_L fm_R = mkBalBranch6 key elt fm_L fm_R

  
mkBalBranch6 key elt fm_L fm_R = 
mkBalBranch5 key elt fm_L fm_R (size_l + size_r < 2) where 
double_L fm_l (Branch key_r elt_r zy (Branch key_rl elt_rl zz fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l zw fm_ll (Branch key_lr elt_lr zx fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
mkBalBranch0 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr) = mkBalBranch02 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)
mkBalBranch00 fm_L fm_R vuu vuv vuw fm_rl fm_rr True = double_L fm_L fm_R
mkBalBranch01 fm_L fm_R vuu vuv vuw fm_rl fm_rr True = single_L fm_L fm_R
mkBalBranch01 fm_L fm_R vuu vuv vuw fm_rl fm_rr False = mkBalBranch00 fm_L fm_R vuu vuv vuw fm_rl fm_rr otherwise
mkBalBranch02 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr) = mkBalBranch01 fm_L fm_R vuu vuv vuw fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)
mkBalBranch1 fm_L fm_R (Branch yz zu zv fm_ll fm_lr) = mkBalBranch12 fm_L fm_R (Branch yz zu zv fm_ll fm_lr)
mkBalBranch10 fm_L fm_R yz zu zv fm_ll fm_lr True = double_R fm_L fm_R
mkBalBranch11 fm_L fm_R yz zu zv fm_ll fm_lr True = single_R fm_L fm_R
mkBalBranch11 fm_L fm_R yz zu zv fm_ll fm_lr False = mkBalBranch10 fm_L fm_R yz zu zv fm_ll fm_lr otherwise
mkBalBranch12 fm_L fm_R (Branch yz zu zv fm_ll fm_lr) = mkBalBranch11 fm_L fm_R yz zu zv fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)
mkBalBranch2 key elt fm_L fm_R True = mkBranch 2 key elt fm_L fm_R
mkBalBranch3 key elt fm_L fm_R True = mkBalBranch1 fm_L fm_R fm_L
mkBalBranch3 key elt fm_L fm_R False = mkBalBranch2 key elt fm_L fm_R otherwise
mkBalBranch4 key elt fm_L fm_R True = mkBalBranch0 fm_L fm_R fm_R
mkBalBranch4 key elt fm_L fm_R False = mkBalBranch3 key elt fm_L fm_R (size_l > sIZE_RATIO * size_r)
mkBalBranch5 key elt fm_L fm_R True = mkBranch 1 key elt fm_L fm_R
mkBalBranch5 key elt fm_L fm_R False = mkBalBranch4 key elt fm_L fm_R (size_r > sIZE_RATIO * size_l)
single_L fm_l (Branch key_r elt_r vux fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l yy fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l = sizeFM fm_L
size_r = sizeFM fm_R

  mkBranch :: Ord b => Int  ->  b  ->  a  ->  FiniteMap b a  ->  FiniteMap b a  ->  FiniteMap b a
mkBranch which key elt fm_l fm_r = 
let 
result = Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r
in result
 where 
balance_ok = True
left_ok = left_ok0 fm_l key fm_l
left_ok0 fm_l key EmptyFM = True
left_ok0 fm_l key (Branch left_key wu wv ww wx) = 
let 
biggest_left_key = fst (findMax fm_l)
in biggest_left_key < key
left_size = sizeFM fm_l
right_ok = right_ok0 fm_r key fm_r
right_ok0 fm_r key EmptyFM = True
right_ok0 fm_r key (Branch right_key vw vx vy vz) = 
let 
smallest_right_key = fst (findMin fm_r)
in key < smallest_right_key
right_size = sizeFM fm_r
unbox :: Int  ->  Int
unbox x = x

  sIZE_RATIO :: Int
sIZE_RATIO = 5

  sizeFM :: FiniteMap a b  ->  Int
sizeFM EmptyFM = 0
sizeFM (Branch yu yv size yw yx) = size

  unitFM :: b  ->  a  ->  FiniteMap b a
unitFM key elt = Branch key elt 1 emptyFM emptyFM


module Maybe where
  import qualified FiniteMap
import qualified Prelude


Let/Where Reductions:
The bindings of the following Let/Where expression
let 
result  = Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r
in result
where 
balance_ok  = True
left_ok  = left_ok0 fm_l key fm_l
left_ok0 fm_l key EmptyFM = True
left_ok0 fm_l key (Branch left_key wu wv ww wx) = 
let 
biggest_left_key  = fst (findMax fm_l)
in biggest_left_key < key
left_size  = sizeFM fm_l
right_ok  = right_ok0 fm_r key fm_r
right_ok0 fm_r key EmptyFM = True
right_ok0 fm_r key (Branch right_key vw vx vy vz) = 
let 
smallest_right_key  = fst (findMin fm_r)
in key < smallest_right_key
right_size  = sizeFM fm_r
unbox x = x

are unpacked to the following functions on top level
mkBranchRight_ok vwx vwy vwz = mkBranchRight_ok0 vwx vwy vwz vwx vwy vwx

mkBranchUnbox vwx vwy vwz x = x

mkBranchLeft_size vwx vwy vwz = sizeFM vwz

mkBranchBalance_ok vwx vwy vwz = True

mkBranchRight_size vwx vwy vwz = sizeFM vwx

mkBranchRight_ok0 vwx vwy vwz fm_r key EmptyFM = True
mkBranchRight_ok0 vwx vwy vwz fm_r key (Branch right_key vw vx vy vz) = key < mkBranchRight_ok0Smallest_right_key fm_r

mkBranchLeft_ok0 vwx vwy vwz fm_l key EmptyFM = True
mkBranchLeft_ok0 vwx vwy vwz fm_l key (Branch left_key wu wv ww wx) = mkBranchLeft_ok0Biggest_left_key fm_l < key

mkBranchLeft_ok vwx vwy vwz = mkBranchLeft_ok0 vwx vwy vwz vwz vwy vwz

The bindings of the following Let/Where expression
let 
result  = Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r
in result

are unpacked to the following functions on top level
mkBranchResult vxu vxv vxw vxx = Branch vxu vxv (mkBranchUnbox vxw vxu vxx (1 + mkBranchLeft_size vxw vxu vxx + mkBranchRight_size vxw vxu vxx)) vxx vxw

The bindings of the following Let/Where expression
mkBalBranch5 key elt fm_L fm_R (size_l + size_r < 2)
where 
double_L fm_l (Branch key_r elt_r zy (Branch key_rl elt_rl zz fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l zw fm_ll (Branch key_lr elt_lr zx fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
mkBalBranch0 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr) = mkBalBranch02 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)
mkBalBranch00 fm_L fm_R vuu vuv vuw fm_rl fm_rr True = double_L fm_L fm_R
mkBalBranch01 fm_L fm_R vuu vuv vuw fm_rl fm_rr True = single_L fm_L fm_R
mkBalBranch01 fm_L fm_R vuu vuv vuw fm_rl fm_rr False = mkBalBranch00 fm_L fm_R vuu vuv vuw fm_rl fm_rr otherwise
mkBalBranch02 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr) = mkBalBranch01 fm_L fm_R vuu vuv vuw fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)
mkBalBranch1 fm_L fm_R (Branch yz zu zv fm_ll fm_lr) = mkBalBranch12 fm_L fm_R (Branch yz zu zv fm_ll fm_lr)
mkBalBranch10 fm_L fm_R yz zu zv fm_ll fm_lr True = double_R fm_L fm_R
mkBalBranch11 fm_L fm_R yz zu zv fm_ll fm_lr True = single_R fm_L fm_R
mkBalBranch11 fm_L fm_R yz zu zv fm_ll fm_lr False = mkBalBranch10 fm_L fm_R yz zu zv fm_ll fm_lr otherwise
mkBalBranch12 fm_L fm_R (Branch yz zu zv fm_ll fm_lr) = mkBalBranch11 fm_L fm_R yz zu zv fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)
mkBalBranch2 key elt fm_L fm_R True = mkBranch 2 key elt fm_L fm_R
mkBalBranch3 key elt fm_L fm_R True = mkBalBranch1 fm_L fm_R fm_L
mkBalBranch3 key elt fm_L fm_R False = mkBalBranch2 key elt fm_L fm_R otherwise
mkBalBranch4 key elt fm_L fm_R True = mkBalBranch0 fm_L fm_R fm_R
mkBalBranch4 key elt fm_L fm_R False = mkBalBranch3 key elt fm_L fm_R (size_l > sIZE_RATIO * size_r)
mkBalBranch5 key elt fm_L fm_R True = mkBranch 1 key elt fm_L fm_R
mkBalBranch5 key elt fm_L fm_R False = mkBalBranch4 key elt fm_L fm_R (size_r > sIZE_RATIO * size_l)
single_L fm_l (Branch key_r elt_r vux fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l yy fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l  = sizeFM fm_L
size_r  = sizeFM fm_R

are unpacked to the following functions on top level
mkBalBranch6Single_L vxy vxz vyu vyv fm_l (Branch key_r elt_r vux fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 vxy vxz fm_l fm_rl) fm_rr

mkBalBranch6MkBalBranch1 vxy vxz vyu vyv fm_L fm_R (Branch yz zu zv fm_ll fm_lr) = mkBalBranch6MkBalBranch12 vxy vxz vyu vyv fm_L fm_R (Branch yz zu zv fm_ll fm_lr)

mkBalBranch6MkBalBranch2 vxy vxz vyu vyv key elt fm_L fm_R True = mkBranch 2 key elt fm_L fm_R

mkBalBranch6MkBalBranch00 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr True = mkBalBranch6Double_L vxy vxz vyu vyv fm_L fm_R

mkBalBranch6MkBalBranch0 vxy vxz vyu vyv fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr) = mkBalBranch6MkBalBranch02 vxy vxz vyu vyv fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)

mkBalBranch6Single_R vxy vxz vyu vyv (Branch key_l elt_l yy fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 vxy vxz fm_lr fm_r)

mkBalBranch6MkBalBranch3 vxy vxz vyu vyv key elt fm_L fm_R True = mkBalBranch6MkBalBranch1 vxy vxz vyu vyv fm_L fm_R fm_L
mkBalBranch6MkBalBranch3 vxy vxz vyu vyv key elt fm_L fm_R False = mkBalBranch6MkBalBranch2 vxy vxz vyu vyv key elt fm_L fm_R otherwise

mkBalBranch6MkBalBranch02 vxy vxz vyu vyv fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr) = mkBalBranch6MkBalBranch01 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)

mkBalBranch6MkBalBranch5 vxy vxz vyu vyv key elt fm_L fm_R True = mkBranch 1 key elt fm_L fm_R
mkBalBranch6MkBalBranch5 vxy vxz vyu vyv key elt fm_L fm_R False = mkBalBranch6MkBalBranch4 vxy vxz vyu vyv key elt fm_L fm_R (mkBalBranch6Size_r vxy vxz vyu vyv > sIZE_RATIO * mkBalBranch6Size_l vxy vxz vyu vyv)

mkBalBranch6MkBalBranch10 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr True = mkBalBranch6Double_R vxy vxz vyu vyv fm_L fm_R

mkBalBranch6Double_L vxy vxz vyu vyv fm_l (Branch key_r elt_r zy (Branch key_rl elt_rl zz fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 vxy vxz fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)

mkBalBranch6Double_R vxy vxz vyu vyv (Branch key_l elt_l zw fm_ll (Branch key_lr elt_lr zx fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 vxy vxz fm_lrr fm_r)

mkBalBranch6Size_l vxy vxz vyu vyv = sizeFM vyu

mkBalBranch6MkBalBranch4 vxy vxz vyu vyv key elt fm_L fm_R True = mkBalBranch6MkBalBranch0 vxy vxz vyu vyv fm_L fm_R fm_R
mkBalBranch6MkBalBranch4 vxy vxz vyu vyv key elt fm_L fm_R False = mkBalBranch6MkBalBranch3 vxy vxz vyu vyv key elt fm_L fm_R (mkBalBranch6Size_l vxy vxz vyu vyv > sIZE_RATIO * mkBalBranch6Size_r vxy vxz vyu vyv)

mkBalBranch6MkBalBranch11 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr True = mkBalBranch6Single_R vxy vxz vyu vyv fm_L fm_R
mkBalBranch6MkBalBranch11 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr False = mkBalBranch6MkBalBranch10 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr otherwise

mkBalBranch6MkBalBranch12 vxy vxz vyu vyv fm_L fm_R (Branch yz zu zv fm_ll fm_lr) = mkBalBranch6MkBalBranch11 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)

mkBalBranch6MkBalBranch01 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr True = mkBalBranch6Single_L vxy vxz vyu vyv fm_L fm_R
mkBalBranch6MkBalBranch01 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr False = mkBalBranch6MkBalBranch00 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr otherwise

mkBalBranch6Size_r vxy vxz vyu vyv = sizeFM vyv

The bindings of the following Let/Where expression
let 
smallest_right_key  = fst (findMin fm_r)
in key < smallest_right_key

are unpacked to the following functions on top level
mkBranchRight_ok0Smallest_right_key vyw = fst (findMin vyw)

The bindings of the following Let/Where expression
let 
biggest_left_key  = fst (findMax fm_l)
in biggest_left_key < key

are unpacked to the following functions on top level
mkBranchLeft_ok0Biggest_left_key vyx = fst (findMax vyx)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed

mainModule FiniteMap
  ((addToFM :: FiniteMap () a  ->  ()  ->  a  ->  FiniteMap () a) :: FiniteMap () a  ->  ()  ->  a  ->  FiniteMap () a)

module FiniteMap where
  import qualified Maybe
import qualified Prelude
  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a) 
  instance (Eq a, Eq b) => Eq (FiniteMap b a) where 
  addToFM :: Ord b => FiniteMap b a  ->  b  ->  a  ->  FiniteMap b a
addToFM fm key elt = addToFM_C addToFM0 fm key elt

  
addToFM0 old new = new

  addToFM_C :: Ord b => (a  ->  a  ->  a)  ->  FiniteMap b a  ->  b  ->  a  ->  FiniteMap b a
addToFM_C combiner EmptyFM key elt = addToFM_C4 combiner EmptyFM key elt
addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt

  
addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt True = Branch new_key (combiner elt new_elt) size fm_l fm_r

  
addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)
addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt otherwise

  
addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r
addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt (new_key > key)

  
addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt (new_key < key)

  
addToFM_C4 combiner EmptyFM key elt = unitFM key elt
addToFM_C4 vvx vvy vvz vwu = addToFM_C3 vvx vvy vvz vwu

  emptyFM :: FiniteMap a b
emptyFM = EmptyFM

  findMax :: FiniteMap a b  ->  (a,b)
findMax (Branch key elt xw xx EmptyFM) = (key,elt)
findMax (Branch key elt xy xz fm_r) = findMax fm_r

  findMin :: FiniteMap a b  ->  (a,b)
findMin (Branch key elt wy EmptyFM wz) = (key,elt)
findMin (Branch key elt xu fm_l xv) = findMin fm_l

  mkBalBranch :: Ord a => a  ->  b  ->  FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
mkBalBranch key elt fm_L fm_R = mkBalBranch6 key elt fm_L fm_R

  
mkBalBranch6 key elt fm_L fm_R = mkBalBranch6MkBalBranch5 key elt fm_L fm_R key elt fm_L fm_R (mkBalBranch6Size_l key elt fm_L fm_R + mkBalBranch6Size_r key elt fm_L fm_R < 2)

  
mkBalBranch6Double_L vxy vxz vyu vyv fm_l (Branch key_r elt_r zy (Branch key_rl elt_rl zz fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 vxy vxz fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)

  
mkBalBranch6Double_R vxy vxz vyu vyv (Branch key_l elt_l zw fm_ll (Branch key_lr elt_lr zx fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 vxy vxz fm_lrr fm_r)

  
mkBalBranch6MkBalBranch0 vxy vxz vyu vyv fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr) = mkBalBranch6MkBalBranch02 vxy vxz vyu vyv fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)

  
mkBalBranch6MkBalBranch00 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr True = mkBalBranch6Double_L vxy vxz vyu vyv fm_L fm_R

  
mkBalBranch6MkBalBranch01 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr True = mkBalBranch6Single_L vxy vxz vyu vyv fm_L fm_R
mkBalBranch6MkBalBranch01 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr False = mkBalBranch6MkBalBranch00 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr otherwise

  
mkBalBranch6MkBalBranch02 vxy vxz vyu vyv fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr) = mkBalBranch6MkBalBranch01 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)

  
mkBalBranch6MkBalBranch1 vxy vxz vyu vyv fm_L fm_R (Branch yz zu zv fm_ll fm_lr) = mkBalBranch6MkBalBranch12 vxy vxz vyu vyv fm_L fm_R (Branch yz zu zv fm_ll fm_lr)

  
mkBalBranch6MkBalBranch10 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr True = mkBalBranch6Double_R vxy vxz vyu vyv fm_L fm_R

  
mkBalBranch6MkBalBranch11 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr True = mkBalBranch6Single_R vxy vxz vyu vyv fm_L fm_R
mkBalBranch6MkBalBranch11 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr False = mkBalBranch6MkBalBranch10 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr otherwise

  
mkBalBranch6MkBalBranch12 vxy vxz vyu vyv fm_L fm_R (Branch yz zu zv fm_ll fm_lr) = mkBalBranch6MkBalBranch11 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)

  
mkBalBranch6MkBalBranch2 vxy vxz vyu vyv key elt fm_L fm_R True = mkBranch 2 key elt fm_L fm_R

  
mkBalBranch6MkBalBranch3 vxy vxz vyu vyv key elt fm_L fm_R True = mkBalBranch6MkBalBranch1 vxy vxz vyu vyv fm_L fm_R fm_L
mkBalBranch6MkBalBranch3 vxy vxz vyu vyv key elt fm_L fm_R False = mkBalBranch6MkBalBranch2 vxy vxz vyu vyv key elt fm_L fm_R otherwise

  
mkBalBranch6MkBalBranch4 vxy vxz vyu vyv key elt fm_L fm_R True = mkBalBranch6MkBalBranch0 vxy vxz vyu vyv fm_L fm_R fm_R
mkBalBranch6MkBalBranch4 vxy vxz vyu vyv key elt fm_L fm_R False = mkBalBranch6MkBalBranch3 vxy vxz vyu vyv key elt fm_L fm_R (mkBalBranch6Size_l vxy vxz vyu vyv > sIZE_RATIO * mkBalBranch6Size_r vxy vxz vyu vyv)

  
mkBalBranch6MkBalBranch5 vxy vxz vyu vyv key elt fm_L fm_R True = mkBranch 1 key elt fm_L fm_R
mkBalBranch6MkBalBranch5 vxy vxz vyu vyv key elt fm_L fm_R False = mkBalBranch6MkBalBranch4 vxy vxz vyu vyv key elt fm_L fm_R (mkBalBranch6Size_r vxy vxz vyu vyv > sIZE_RATIO * mkBalBranch6Size_l vxy vxz vyu vyv)

  
mkBalBranch6Single_L vxy vxz vyu vyv fm_l (Branch key_r elt_r vux fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 vxy vxz fm_l fm_rl) fm_rr

  
mkBalBranch6Single_R vxy vxz vyu vyv (Branch key_l elt_l yy fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 vxy vxz fm_lr fm_r)

  
mkBalBranch6Size_l vxy vxz vyu vyv = sizeFM vyu

  
mkBalBranch6Size_r vxy vxz vyu vyv = sizeFM vyv

  mkBranch :: Ord b => Int  ->  b  ->  a  ->  FiniteMap b a  ->  FiniteMap b a  ->  FiniteMap b a
mkBranch which key elt fm_l fm_r = mkBranchResult key elt fm_r fm_l

  
mkBranchBalance_ok vwx vwy vwz = True

  
mkBranchLeft_ok vwx vwy vwz = mkBranchLeft_ok0 vwx vwy vwz vwz vwy vwz

  
mkBranchLeft_ok0 vwx vwy vwz fm_l key EmptyFM = True
mkBranchLeft_ok0 vwx vwy vwz fm_l key (Branch left_key wu wv ww wx) = mkBranchLeft_ok0Biggest_left_key fm_l < key

  
mkBranchLeft_ok0Biggest_left_key vyx = fst (findMax vyx)

  
mkBranchLeft_size vwx vwy vwz = sizeFM vwz

  
mkBranchResult vxu vxv vxw vxx = Branch vxu vxv (mkBranchUnbox vxw vxu vxx (1 + mkBranchLeft_size vxw vxu vxx + mkBranchRight_size vxw vxu vxx)) vxx vxw

  
mkBranchRight_ok vwx vwy vwz = mkBranchRight_ok0 vwx vwy vwz vwx vwy vwx

  
mkBranchRight_ok0 vwx vwy vwz fm_r key EmptyFM = True
mkBranchRight_ok0 vwx vwy vwz fm_r key (Branch right_key vw vx vy vz) = key < mkBranchRight_ok0Smallest_right_key fm_r

  
mkBranchRight_ok0Smallest_right_key vyw = fst (findMin vyw)

  
mkBranchRight_size vwx vwy vwz = sizeFM vwx

  mkBranchUnbox :: Ord a =>  ->  (FiniteMap a b) ( ->  a ( ->  (FiniteMap a b) (Int  ->  Int)))
mkBranchUnbox vwx vwy vwz x = x

  sIZE_RATIO :: Int
sIZE_RATIO = 5

  sizeFM :: FiniteMap a b  ->  Int
sizeFM EmptyFM = 0
sizeFM (Branch yu yv size yw yx) = size

  unitFM :: a  ->  b  ->  FiniteMap a b
unitFM key elt = Branch key elt 1 emptyFM emptyFM


module Maybe where
  import qualified FiniteMap
import qualified Prelude


Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow

mainModule FiniteMap
  (addToFM :: FiniteMap () a  ->  ()  ->  a  ->  FiniteMap () a)

module FiniteMap where
  import qualified Maybe
import qualified Prelude
  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a) 
  instance (Eq a, Eq b) => Eq (FiniteMap a b) where 
  addToFM :: Ord b => FiniteMap b a  ->  b  ->  a  ->  FiniteMap b a
addToFM fm key elt = addToFM_C addToFM0 fm key elt

  
addToFM0 old new = new

  addToFM_C :: Ord b => (a  ->  a  ->  a)  ->  FiniteMap b a  ->  b  ->  a  ->  FiniteMap b a
addToFM_C combiner EmptyFM key elt = addToFM_C4 combiner EmptyFM key elt
addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt

  
addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt True = Branch new_key (combiner elt new_elt) size fm_l fm_r

  
addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)
addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt otherwise

  
addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r
addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt (new_key > key)

  
addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt (new_key < key)

  
addToFM_C4 combiner EmptyFM key elt = unitFM key elt
addToFM_C4 vvx vvy vvz vwu = addToFM_C3 vvx vvy vvz vwu

  emptyFM :: FiniteMap b a
emptyFM = EmptyFM

  findMax :: FiniteMap b a  ->  (b,a)
findMax (Branch key elt xw xx EmptyFM) = (key,elt)
findMax (Branch key elt xy xz fm_r) = findMax fm_r

  findMin :: FiniteMap b a  ->  (b,a)
findMin (Branch key elt wy EmptyFM wz) = (key,elt)
findMin (Branch key elt xu fm_l xv) = findMin fm_l

  mkBalBranch :: Ord a => a  ->  b  ->  FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
mkBalBranch key elt fm_L fm_R = mkBalBranch6 key elt fm_L fm_R

  
mkBalBranch6 key elt fm_L fm_R = mkBalBranch6MkBalBranch5 key elt fm_L fm_R key elt fm_L fm_R (mkBalBranch6Size_l key elt fm_L fm_R + mkBalBranch6Size_r key elt fm_L fm_R < Pos (Succ (Succ Zero)))

  
mkBalBranch6Double_L vxy vxz vyu vyv fm_l (Branch key_r elt_r zy (Branch key_rl elt_rl zz fm_rll fm_rlr) fm_rr) = mkBranch (Pos (Succ (Succ (Succ (Succ (Succ Zero)))))) key_rl elt_rl (mkBranch (Pos (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))) vxy vxz fm_l fm_rll) (mkBranch (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))) key_r elt_r fm_rlr fm_rr)

  
mkBalBranch6Double_R vxy vxz vyu vyv (Branch key_l elt_l zw fm_ll (Branch key_lr elt_lr zx fm_lrl fm_lrr)) fm_r = mkBranch (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))) key_lr elt_lr (mkBranch (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))) key_l elt_l fm_ll fm_lrl) (mkBranch (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))) vxy vxz fm_lrr fm_r)

  
mkBalBranch6MkBalBranch0 vxy vxz vyu vyv fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr) = mkBalBranch6MkBalBranch02 vxy vxz vyu vyv fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)

  
mkBalBranch6MkBalBranch00 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr True = mkBalBranch6Double_L vxy vxz vyu vyv fm_L fm_R

  
mkBalBranch6MkBalBranch01 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr True = mkBalBranch6Single_L vxy vxz vyu vyv fm_L fm_R
mkBalBranch6MkBalBranch01 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr False = mkBalBranch6MkBalBranch00 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr otherwise

  
mkBalBranch6MkBalBranch02 vxy vxz vyu vyv fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr) = mkBalBranch6MkBalBranch01 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr (sizeFM fm_rl < Pos (Succ (Succ Zero)) * sizeFM fm_rr)

  
mkBalBranch6MkBalBranch1 vxy vxz vyu vyv fm_L fm_R (Branch yz zu zv fm_ll fm_lr) = mkBalBranch6MkBalBranch12 vxy vxz vyu vyv fm_L fm_R (Branch yz zu zv fm_ll fm_lr)

  
mkBalBranch6MkBalBranch10 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr True = mkBalBranch6Double_R vxy vxz vyu vyv fm_L fm_R

  
mkBalBranch6MkBalBranch11 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr True = mkBalBranch6Single_R vxy vxz vyu vyv fm_L fm_R
mkBalBranch6MkBalBranch11 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr False = mkBalBranch6MkBalBranch10 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr otherwise

  
mkBalBranch6MkBalBranch12 vxy vxz vyu vyv fm_L fm_R (Branch yz zu zv fm_ll fm_lr) = mkBalBranch6MkBalBranch11 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr (sizeFM fm_lr < Pos (Succ (Succ Zero)) * sizeFM fm_ll)

  
mkBalBranch6MkBalBranch2 vxy vxz vyu vyv key elt fm_L fm_R True = mkBranch (Pos (Succ (Succ Zero))) key elt fm_L fm_R

  
mkBalBranch6MkBalBranch3 vxy vxz vyu vyv key elt fm_L fm_R True = mkBalBranch6MkBalBranch1 vxy vxz vyu vyv fm_L fm_R fm_L
mkBalBranch6MkBalBranch3 vxy vxz vyu vyv key elt fm_L fm_R False = mkBalBranch6MkBalBranch2 vxy vxz vyu vyv key elt fm_L fm_R otherwise

  
mkBalBranch6MkBalBranch4 vxy vxz vyu vyv key elt fm_L fm_R True = mkBalBranch6MkBalBranch0 vxy vxz vyu vyv fm_L fm_R fm_R
mkBalBranch6MkBalBranch4 vxy vxz vyu vyv key elt fm_L fm_R False = mkBalBranch6MkBalBranch3 vxy vxz vyu vyv key elt fm_L fm_R (mkBalBranch6Size_l vxy vxz vyu vyv > sIZE_RATIO * mkBalBranch6Size_r vxy vxz vyu vyv)

  
mkBalBranch6MkBalBranch5 vxy vxz vyu vyv key elt fm_L fm_R True = mkBranch (Pos (Succ Zero)) key elt fm_L fm_R
mkBalBranch6MkBalBranch5 vxy vxz vyu vyv key elt fm_L fm_R False = mkBalBranch6MkBalBranch4 vxy vxz vyu vyv key elt fm_L fm_R (mkBalBranch6Size_r vxy vxz vyu vyv > sIZE_RATIO * mkBalBranch6Size_l vxy vxz vyu vyv)

  
mkBalBranch6Single_L vxy vxz vyu vyv fm_l (Branch key_r elt_r vux fm_rl fm_rr) = mkBranch (Pos (Succ (Succ (Succ Zero)))) key_r elt_r (mkBranch (Pos (Succ (Succ (Succ (Succ Zero))))) vxy vxz fm_l fm_rl) fm_rr

  
mkBalBranch6Single_R vxy vxz vyu vyv (Branch key_l elt_l yy fm_ll fm_lr) fm_r = mkBranch (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))) key_l elt_l fm_ll (mkBranch (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))) vxy vxz fm_lr fm_r)

  
mkBalBranch6Size_l vxy vxz vyu vyv = sizeFM vyu

  
mkBalBranch6Size_r vxy vxz vyu vyv = sizeFM vyv

  mkBranch :: Ord b => Int  ->  b  ->  a  ->  FiniteMap b a  ->  FiniteMap b a  ->  FiniteMap b a
mkBranch which key elt fm_l fm_r = mkBranchResult key elt fm_r fm_l

  
mkBranchBalance_ok vwx vwy vwz = True

  
mkBranchLeft_ok vwx vwy vwz = mkBranchLeft_ok0 vwx vwy vwz vwz vwy vwz

  
mkBranchLeft_ok0 vwx vwy vwz fm_l key EmptyFM = True
mkBranchLeft_ok0 vwx vwy vwz fm_l key (Branch left_key wu wv ww wx) = mkBranchLeft_ok0Biggest_left_key fm_l < key

  
mkBranchLeft_ok0Biggest_left_key vyx = fst (findMax vyx)

  
mkBranchLeft_size vwx vwy vwz = sizeFM vwz

  
mkBranchResult vxu vxv vxw vxx = Branch vxu vxv (mkBranchUnbox vxw vxu vxx (Pos (Succ Zero) + mkBranchLeft_size vxw vxu vxx + mkBranchRight_size vxw vxu vxx)) vxx vxw

  
mkBranchRight_ok vwx vwy vwz = mkBranchRight_ok0 vwx vwy vwz vwx vwy vwx

  
mkBranchRight_ok0 vwx vwy vwz fm_r key EmptyFM = True
mkBranchRight_ok0 vwx vwy vwz fm_r key (Branch right_key vw vx vy vz) = key < mkBranchRight_ok0Smallest_right_key fm_r

  
mkBranchRight_ok0Smallest_right_key vyw = fst (findMin vyw)

  
mkBranchRight_size vwx vwy vwz = sizeFM vwx

  mkBranchUnbox :: Ord a =>  ->  (FiniteMap a b) ( ->  a ( ->  (FiniteMap a b) (Int  ->  Int)))
mkBranchUnbox vwx vwy vwz x = x

  sIZE_RATIO :: Int
sIZE_RATIO = Pos (Succ (Succ (Succ (Succ (Succ Zero)))))

  sizeFM :: FiniteMap a b  ->  Int
sizeFM EmptyFM = Pos Zero
sizeFM (Branch yu yv size yw yx) = size

  unitFM :: a  ->  b  ->  FiniteMap a b
unitFM key elt = Branch key elt (Pos (Succ Zero)) emptyFM emptyFM


module Maybe where
  import qualified FiniteMap
import qualified Prelude


Haskell To QDPs